(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 9))
(assert (let ((e1(_ bv21168 15)))
(let ((e2 (bvmul v0 v0)))
(let ((e3 (bvsrem e2 v0)))
(let ((e4 (bvsdiv v0 e3)))
(let ((e5 (bvxnor e4 e3)))
(let ((e6 (bvneg e2)))
(let ((e7 (ite (= e6 e5) (_ bv1 1) (_ bv0 1))))
(let ((e8 (bvnot e7)))
(let ((e9 (bvnand e4 e4)))
(let ((e10 (bvmul ((_ sign_extend 8) e7) e4)))
(let ((e11 (ite (bvuge e5 e2) (_ bv1 1) (_ bv0 1))))
(let ((e12 ((_ sign_extend 5) e9)))
(let ((e13 ((_ rotate_right 8) e9)))
(let ((e14 (bvudiv e7 e7)))
(let ((e15 (bvmul e5 e10)))
(let ((e16 (bvand e9 ((_ sign_extend 8) e7))))
(let ((e17 (bvadd ((_ sign_extend 8) e8) e9)))
(let ((e18 (bvnand e3 e4)))
(let ((e19 (bvsub ((_ zero_extend 8) e7) e2)))
(let ((e20 (bvcomp e19 e9)))
(let ((e21 (ite (bvuge e1 ((_ zero_extend 1) e12)) (_ bv1 1) (_ bv0 1))))
(let ((e22 (bvuge e12 ((_ zero_extend 5) e2))))
(let ((e23 (bvsgt e17 e16)))
(let ((e24 (bvule e1 ((_ sign_extend 6) e2))))
(let ((e25 (bvugt e17 e19)))
(let ((e26 (bvslt e2 ((_ sign_extend 8) e14))))
(let ((e27 (bvugt e19 e17)))
(let ((e28 (bvuge e14 e20)))
(let ((e29 (bvult e18 e10)))
(let ((e30 (bvugt e2 v0)))
(let ((e31 (bvsgt e15 e13)))
(let ((e32 (bvuge e10 ((_ zero_extend 8) e20))))
(let ((e33 (distinct ((_ sign_extend 6) e15) e1)))
(let ((e34 (bvuge e3 ((_ zero_extend 8) e11))))
(let ((e35 (bvuge ((_ zero_extend 8) e14) e5)))
(let ((e36 (bvult ((_ zero_extend 8) e7) e18)))
(let ((e37 (bvule e12 ((_ sign_extend 5) e5))))
(let ((e38 (bvule e9 e19)))
(let ((e39 (distinct e10 e15)))
(let ((e40 (bvsge e6 e16)))
(let ((e41 (bvsgt e17 e18)))
(let ((e42 (bvule e6 ((_ zero_extend 8) e21))))
(let ((e43 (bvuge e9 e10)))
(let ((e44 (bvugt e11 e14)))
(let ((e45 (bvsgt e12 ((_ zero_extend 13) e14))))
(let ((e46 (bvuge e5 e10)))
(let ((e47 (bvult e3 ((_ zero_extend 8) e8))))
(let ((e48 (bvsle e17 e9)))
(let ((e49 (= e1 ((_ sign_extend 6) e19))))
(let ((e50 (= e17 ((_ sign_extend 8) e7))))
(let ((e51 (bvsge e1 ((_ sign_extend 6) v0))))
(let ((e52 (bvule e5 e3)))
(let ((e53 (bvsge ((_ zero_extend 8) e11) e15)))
(let ((e54 (bvsle e15 e16)))
(let ((e55 (bvsle ((_ sign_extend 8) e11) e16)))
(let ((e56 (distinct v0 e10)))
(let ((e57 (bvuge e19 e18)))
(let ((e58 (= e10 e13)))
(let ((e59 (bvslt e15 ((_ zero_extend 8) e11))))
(let ((e60 (bvuge e7 e7)))
(let ((e61 (bvult e19 e9)))
(let ((e62 (bvugt e17 ((_ zero_extend 8) e7))))
(let ((e63 (bvsle ((_ zero_extend 8) e11) e15)))
(let ((e64 (bvsle e3 e18)))
(let ((e65 (bvsgt e18 ((_ zero_extend 8) e8))))
(let ((e66 (bvslt ((_ zero_extend 8) e7) e2)))
(let ((e67 (distinct ((_ zero_extend 8) e20) e5)))
(let ((e68 (bvslt v0 e18)))
(let ((e69 (distinct ((_ zero_extend 6) e10) e1)))
(let ((e70 (bvsgt v0 e3)))
(let ((e71 (bvslt e12 ((_ zero_extend 5) e2))))
(let ((e72 (distinct e12 e12)))
(let ((e73 (bvugt ((_ zero_extend 5) e17) e12)))
(let ((e74 (bvule ((_ zero_extend 8) e14) e19)))
(let ((e75 (bvslt e4 e2)))
(let ((e76 (or e42 e52)))
(let ((e77 (xor e30 e33)))
(let ((e78 (= e73 e43)))
(let ((e79 (= e26 e71)))
(let ((e80 (ite e67 e51 e29)))
(let ((e81 (= e36 e56)))
(let ((e82 (ite e44 e81 e65)))
(let ((e83 (=> e54 e70)))
(let ((e84 (not e39)))
(let ((e85 (xor e66 e82)))
(let ((e86 (or e37 e63)))
(let ((e87 (=> e62 e72)))
(let ((e88 (=> e49 e53)))
(let ((e89 (and e78 e28)))
(let ((e90 (xor e35 e83)))
(let ((e91 (=> e22 e84)))
(let ((e92 (ite e80 e79 e80)))
(let ((e93 (=> e46 e27)))
(let ((e94 (and e45 e55)))
(let ((e95 (=> e69 e41)))
(let ((e96 (not e89)))
(let ((e97 (=> e61 e94)))
(let ((e98 (ite e50 e31 e93)))
(let ((e99 (xor e23 e34)))
(let ((e100 (= e60 e88)))
(let ((e101 (=> e57 e77)))
(let ((e102 (=> e47 e76)))
(let ((e103 (not e100)))
(let ((e104 (and e103 e24)))
(let ((e105 (and e92 e102)))
(let ((e106 (=> e90 e98)))
(let ((e107 (=> e86 e99)))
(let ((e108 (or e74 e85)))
(let ((e109 (not e96)))
(let ((e110 (or e107 e105)))
(let ((e111 (ite e108 e38 e64)))
(let ((e112 (ite e91 e91 e40)))
(let ((e113 (and e25 e97)))
(let ((e114 (ite e95 e101 e101)))
(let ((e115 (and e58 e68)))
(let ((e116 (or e104 e104)))
(let ((e117 (= e32 e113)))
(let ((e118 (xor e112 e109)))
(let ((e119 (or e118 e115)))
(let ((e120 (= e48 e117)))
(let ((e121 (xor e111 e59)))
(let ((e122 (=> e75 e116)))
(let ((e123 (not e119)))
(let ((e124 (=> e110 e121)))
(let ((e125 (xor e124 e123)))
(let ((e126 (ite e120 e114 e120)))
(let ((e127 (or e87 e106)))
(let ((e128 (or e126 e122)))
(let ((e129 (ite e128 e125 e125)))
(let ((e130 (= e129 e127)))
(let ((e131 (and e130 (not (= e3 (_ bv0 9))))))
(let ((e132 (and e131 (not (= e3 (bvnot (_ bv0 9)))))))
(let ((e133 (and e132 (not (= v0 (_ bv0 9))))))
(let ((e134 (and e133 (not (= v0 (bvnot (_ bv0 9)))))))
(let ((e135 (and e134 (not (= e7 (_ bv0 1))))))
e135
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
